COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	PROTOCOL FOR EXAMPLE IN REPORT.2[APG,DCL]
C00006 00003	Protocol for  Finite Binary Tree.
C00010 00004	Protocol for Iterative Factorial
C00013 00005	Protocol for unify.
C00014 ENDMK
C⊗;
PROTOCOL FOR EXAMPLE IN REPORT.2[APG,DCL]

FRAME

Procedure:  standon

At(x,y)∧At(z,y)∧Robot(x)∧Box(z){standon(x,z)}On(x,z);

Procedure:  step-up

Robot(x)∧Box(y)∧Box(z)∧On(x,y)∧Stacked(z,y){step-up(x,y,z)}On(x,z);

Axiom: Robot(x)∧On(x,y)∧¬Stacked(z,y) ⊃ Ontop(x);

Initial State:
Robot(M)∧Box(B1)∧Box(B2)∧Box(B3)∧At(B1,L)∧Stacked(B2,B1)∧Stacked(B3,B2)

Goal State:
Ontop(M);

Give iterative solution;

**********************
Structure of solution:

Request for an iterative solution requires the application of VCGEN-rule, V4:

Initial-state{A}R,  R∧S{B}R,  R∧¬S⊃Ontop(M)
------------------------------------
Initial-state{A;R; while S do B} Ontop(M)


First, attempt to satisfy R∧¬S⊃Ontop(M); only Axiom is applicable.
There are choices for R and S, but the correct ones are:

	R: Robot(M)∧On(M,y); S: Stacked(z,y);

This expands the instance of V4 to:

I-S{A}Robot(M)∧On(M,y), 					(1)

	Robot(M)∧On(M,y)∧Stacked(z,y){B}Robot(M)∧On(M,y),	(2)

		Robot(M)∧On(M,y)∧¬Stacked(z,y)⊃Ontop(M);	(3)
--------------------------------------------------------
I-S{A;Robot(M)∧On(M,y); while Stacked(z,y) do B} Ontop(M)

(3) is Axiom.

(2) almost matches Procedure:stepup.  The match can be made by using
VCGEN-rule V1 on stepup:

Robot(x)∧On(x,y)∧Stacked(z,y){step-up(x,y,z)}On(x,z)
----------------------------------------------------
Robot(x)∧On(x,y)∧Stacked(z,y){step-up(x,y,z);y←z}On(x,y)

Substituting M for x in the above, and substituting  step-up(M,y,z);y←z for 
B in (2) gives:

I-S{A}Robot(M)∧On(M,y),							(4)

	Robot(M)∧On(M,y)∧Stacked(z,y){step-up(M,y,z);y←z}On(M,y),	(5)

		Robot(M)∧On(M,y)∧¬Stacked(z,y)⊃Ontop(M);		(6)
--------------------------------------------------------
I-S{A;Robot(M)∧On(M,y); while Stacked(z,y) do(step-up(M,y,z);y←z)}Ontop(M)


Similarly, attacking (4) will lead to:

I-S{prog for standon conditional}Robot(M)∧On(M,B1).

Applying V1 yields (4):

I-S{prog for standon conditional}Robot(M)∧On(M,B1)
--------------------------------------------------
I-S{prog for standon conditional; y←B1}Robot(M)∧On(M,y)

The final program is thus:
prog for standon conditional; y←B1; while Stacked(z,y) do(step-up(M,y,z);y←z)

Protocol for  Finite Binary Tree.

Def1: FB(t) ≡ t=null ∨ (FB(car(t))∧FB(cdr(t)))

Ax1: t=null ⊃ ord(t)=0

Ax2: t≠null∧ord(car(t))≥ ord(cdr(t)) ⊃ ord(t)=ord(car(t))+1

Ax3: t≠null∧ord(car(t))<ord(cdr(t)) ⊃ ord(t)=ord(cdr(t))+1

Given Fb(t) construct a recursive procedure,fb(r,t) such that r=ord(t);

************

Problem statement forces application of rule V8:

FB(t){fb(r,t)}r=ord(t) ||- FB(t){A}r=ord(t)	(1) ||-(2)
-------------------------------------------     ----------
FB(t){proc fb(r,t);A}r=ord(t)			   (3)

Assume (1); attempt(2) using V5, the conditional rule.

Thus replace "A" by "A; if Q then B else C";(2) expands to;

FB(t){A;Q-if;B}r=ord(t),  FB(t){A;¬Q-if;C} r=ord(t)    (4) , (5)
------------------------------------------------       ---------
      FB(t){A; if Q then B else C}r=ord(t) 		  (6)

Natural choice of Q-if is: t =null; reasonable attempt at A is null; this,
combined with  a B of r←0 gives:

FB(t){t=null;r←0}r=ord(t),  FB(t){¬t=null;C} r=ord(t)   (7) , (8)
-----------------------------------------------------   ---------
	FB(t){if t=null then r←0 else C}r=ord(t)           (9)

(7) reduces to: FB(t)∧t=null ⊃0=ord(t) which is provable.

(8)is more difficult. A reasonable argument for C can be made as follows:
since we assume that t≠null, and FB(t), we have by Def1,

	FB(car(t))∧and FB(cdr(t)). Since we are assuming (1) we have
	FB(car(t)){fb(r1,(car(t)))}r1=ord(car(t)) and,
	FB(cdr(t)){fb(r2,(cdr(t)))}r2=ord(cdr(t)).

Substituting into AX2 and AX3 gives:

Ax2': t≠null∧r1≥r2 ⊃ ord(t)=r1+1
Ax3': t≠null∧r1<r2 ⊃ ord(t)=r2+1


All this suggests the following for C in (8):
(***note***: an example has not been used in the above arguments; use of
an example perhaps will make the derivation of C more palitable.)

C: fb(r1,(car(t)));fb(r2,(cdr(t)));if r1≥r2 then r←r1+1 else r←r2+1

This choice of C is correct  and can be tediously verified.




Protocol for Iterative Factorial

Write an iterative procedure named fact, with input parameter named a,
output variable named r. The value of a is always ≥0; the value of r
is to be a!.

******
Above will give rise to the following chain of events:

First V8:
a≥0{fact(r,a)}r=a! ||- a≥0{A}r=a!      (1) ||- (2)
--------------------------------       -----------
    a≥0{proc fact(r,a);A}r=a!             (3)

Expand A by V4 in (2):

a≥0{A}R, R∧S{B}R, R∧¬S⊃r=a!      (4), (5), (6)

(3) becomes: a≥0{proc fact(r,a);A;R; while S do B} r=a!    (7).

Pick a new variable,x; let S be x≠0;

a≥0{A}R, R∧x≠0{B}R, R∧x=0⊃r=a!  		(8), (9), (10)
a≥0{proc fact(r,a);A;R; while x≠0 do B;} r=a!  (11).

Let R be r*x!=a!.

a≥0{A}r*x!=a!, r*x!=a!∧x≠0{B}r*x!=a!, r*x!=a!∧x=0⊃r=a!. (12), (13), (14)
a≥0{proc fact(r,a);A;r*x!=a!; while x≠0 do B;}r=a!      (15)

(12) is to be the initial case.  Let A be x←a; r←1;
This reduces (12) to a≥0⊃1*a!=a!.

Consider (13). B must reduce x.  Let B be C; x←x-1
(13) becomes:
r*x!=a!∧x≠0{C}r*(x-1)!=a!	(16).

Let C be r←r*x in (16), giving, after simplification:
r*x!=a!∧x≠0 ⊃ (r*x)*(x-1)!=a!   (17).

(17) simplifies to a true premise.

Thus the final program is:
	proc fact(r,a) x←a;r←1; while x≠0 do (r←r*x; x←x-1)


Protocol for unify.

Construct a procedure,unify(x,y). x and y are two lists of equal 
length.  The output variable, z, will either be  NIL or